Nuprl Lemma : decl-rename-cap
0,22
postcript
pdf
r
:(Id
Id),
f
:
a
:Id fp
Type,
a
:Id,
z
:Type.
Inj(Id; Id;
r
)
rename(
r
;
f
)(
r
(
a
))?
z
=
f
(
a
)?
z
Type
latex
Definitions
lexpr{i}
,
Id
,
IdDeq
,
x
:
A
.
B
(
x
)
,
t
T
Lemmas
id-deq
wf
,
Id
wf
,
fpf-rename-cap
origin
r:(Id
Id), f:a:Id fp Type, a:Id, z:Type.
rename(r;f)(r(a))?z = f(a)?z 
Type r:(IdId), f:a:Id fp Type, a:Id, z:Type.
rename(r;f)(r(a))?z = f(a)?z Type x:A. B(x) T